import Data.List  
import Data.Char    
import Control.Monad
import Maybe        

import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import qualified Text.ParserCombinators.Parsec.Token as P
import Text.ParserCombinators.Parsec.Language 

data Term = Var String | Param String [String] | Bound Int | Fun String [Term] deriving Eq

data Form = Pred String [Term] | Conn String [Form] | Quant String String Form deriving Eq

type Goal = ([Form],[Form]) 

precOf :: String -> Int
precOf op = maybe (-1) id $ lookup op table
    where table = [("~",4),("&",3),("|",2),("<->",1),("-->",1)]

instance Show Term where
    show (Var x)     = '?':x
    show (Param x _) = x
    show (Bound i)   = error "unmatched index"
    show (Fun f [])  = f
    show (Fun f ts)  = f ++ enclose (map show ts)

instance Show Form where
    showsPrec _ (Pred p []) = showString p 
    showsPrec _ (Pred p ts) = showString p . showString (enclose (map show ts))
    showsPrec _ (Conn "~" [p]) = showString "~" . showsPrec (precOf "~") p
    showsPrec k (Conn c [p,q]) 
        = showParen (pc <= k) $ showsPrec (max pc k) p
          . showString (" "++c++" ") . showsPrec (max pc k) q
        where pc = precOf c
    showsPrec k (Quant qnt b p) 
        = showParen (k>0) $ showString (qnt++" "++ b ++ ". ")
          . showsPrec 0 (subst 0 (Fun b []) p)
    showsPrec _ _ = error "unknown formula"

enclose ss = concat ["(",intercalate ", " ss,")"]

showGoal :: Int -> Goal -> String
showGoal n (ps,qs) =  concat [" ",show n,". ", formlist ps," |- ",formlist qs]
    where formlist [] = "empty"
          formlist ts = intercalate "," (map show ts)

replace :: Term -> Term -> Term -> Term
replace u1 u2 t
    = if t==u1 
      then u2 
      else case t of 
             (Fun a ts) -> Fun a (map (replace u1 u2) ts)
             _          -> t

abstract :: Int -> Term -> Form -> Form
abstract i t (Pred a ts)     = Pred a (map (replace t (Bound i)) ts)
abstract i t (Conn b ps)     = Conn b (map (abstract i t) ps)
abstract i t (Quant qnt b p) = Quant qnt b (abstract (i+1) t p)

subst :: Int -> Term -> Form -> Form
subst i t (Pred a ts)     = Pred a (map (replace (Bound i) t) ts)
subst i t (Conn b ps)     = Conn b (map (subst i t) ps)
subst i t (Quant qnt b p) = Quant qnt b (subst (i+1) t p)

accumForm :: (Term -> a -> a) -> Form -> a -> a
accumForm f (Pred _ ts)   z = foldr f z ts
accumForm f (Conn _ ps)   z = foldr (accumForm f) z ps
accumForm f (Quant _ _ p) z = accumForm f p z

accumGoal :: (Form -> a -> a) -> Goal -> a -> a
accumGoal f (ps,qs) z = foldr f (foldr f z qs) ps

termVars :: Term -> [String] -> [String]
termVars (Var a)    bs = insert a bs
termVars (Fun _ ts) bs = foldr termVars bs ts
termVars _          bs = bs

termParams :: Term -> [(String, [String])] -> [(String, [String])]
termParams (Param a bs) pairs = (a,bs):pairs
termParams (Fun _ ts)   pairs = foldr termParams pairs ts
termParams _            pairs = pairs

goalVars :: Goal -> [String]  -- Slight change from Paulson
goalVars g = accumGoal (accumForm termVars) g []

goalParams :: Goal -> [(String, [String])] -> [(String, [String])]
goalParams = accumGoal (accumForm termParams)

lexer  = P.makeTokenParser funDef
funDef = emptyDef 
         { P.identStart      = letter 
         , P.identLetter     = alphaNum
         , P.reservedNames   = [ "ALL", "EX"]
         , P.reservedOpNames = [ "?","~","&","|","<->","-->","."]
         , P.caseSensitive   = True   
         }

commaSep   = P.commaSep   lexer  
identifier = P.identifier lexer    
parens     = P.parens     lexer    
reserved   = P.reserved   lexer    
reservedOp = P.reservedOp lexer

termpack   = parens(commaSep term) <|> return [] 
term       = param <|> appl Fun
param      = do { reservedOp "?"; x <- identifier; return (Var x) }

form       = quanti "ALL" <|> quanti "EX" <|> expr
expr       = disj `chainr1` (binOp "-->" <|> binOp "<->")
disj       = conj `chainr1` (binOp "|")
conj       = prim `chainr1` (binOp "&")
prim       = uniOp "~" <|> parens(form) <|> appl Pred

appl :: (String -> [Term] -> a) -> GenParser Char st a
appl cons  = do { p <- identifier; args  <- termpack; return (cons p args) }

quanti qnt = do { reserved qnt ; b <- identifier ; reservedOp "." ; f <- form
                ; return (Quant qnt b (abstract 0 (Fun b []) f)) }
uniOp op   = do { reservedOp op ; f <- prim ; return (Conn op [f]) }
binOp op   = do { reservedOp op ; return (\lft rght -> Conn op [lft,rght]) }

parseForm  = parse form "Paulson" 
type Env = [(String,Term)]

unifyLists :: Env -> [Term] -> [Term] -> Maybe Env
unifyLists env = unifyl
    where
      chase :: Term -> Term
      chase (Var a) = maybe (Var a) chase (lookup a env)
      chase t       = t
      --
      occurs :: String -> Term -> Bool
      occurs a (Fun _ ts)   = any (occurs a) ts
      occurs a (Param _ bs) = any ((occurs a) . Var) bs
      occurs a (Var b)      = (a==b)
                            || maybe False (occurs a) (lookup b env)
      occurs a _ = False
      --
      unify :: Term -> Term -> Maybe Env
      unify v@(Var a) t 
          | t==v        = Just env
          | occurs a t  = Nothing
          | otherwise   = Just ((a,t):env)
      unify t v@(Var _) = unify v t
      unify (Param a _) (Param b _)
          | a==b        = Just env
          | otherwise   = Nothing
      unify (Fun a ts) (Fun b us)
          | a==b        = unifyl ts us
          | otherwise   = Nothing
      unify _ _         = Nothing
      --
      unifyl :: [Term] -> [Term] -> Maybe Env
      unifyl [] [] = Just env
      unifyl (t:ts) (u:us) 
                   = do e <- unify (chase t) (chase u) 
                        unifyLists e ts us
      unifyl _ _   = Nothing

atoms :: Form -> Form -> Maybe Env
atoms (Pred a ts) (Pred b us)
    = if a==b then unifyLists [] ts us else Nothing
atoms _ _ = Nothing

instTerm :: Env -> Term -> Term
instForm :: Env -> Form -> Form
instGoal :: Env -> Goal -> Goal

instTerm env (Fun a ts)   = Fun a (map (instTerm env) ts)
instTerm env (Param a bs) = Param a (foldr termVars [] 
                                     (map ((instTerm env) . Var) bs))
instTerm env (Var a)      = maybe (Var a) (instTerm env) (lookup a env)
instTerm env t            = t

instForm env (Pred a ts)     = Pred a (map (instTerm env) ts)
instForm env (Conn b ps)     = Conn b (map (instForm env) ps)
instForm env (Quant qnt b p) = Quant qnt b (instForm env p)

instGoal env (ps,qs) = (map (instForm env) ps, map (instForm env) qs)

unifiable (ps,qs) = catMaybes [atoms p q | p<- ps, q <- qs]

spliceGoals gs newgs i = take (i-1) gs ++ newgs ++ drop i gs

data PState = PState [Goal] Form Int

nth [] _     = Nothing
nth (x:_)  0 = Just x
nth (_:xs) i = nth xs (i-1)

inst env gs p n = PState [instGoal env g | g <- gs] (instForm env p) n

unify i (PState gs p n) = maybe [] id ps
    where ps = do { g <- nth gs (i-1)
                  ; Just [next env | env <- unifiable g]
                  }
          next env = inst env (spliceGoals gs [] i) p n 


